es:ES, l:IdLnk, tg:Id, P, Q:({e:E| loc(e) = source(l)  Id }Prop), B:Type, ds:x:Id fp Type,
f:({e:E| loc(e) = source(l)  Id }B).
(e:{e:E| loc(e) = source(l)  Id }. P(e)  Q(e))
 (es-sends-iff2(es;l;tg;B;ds;e.P(e);e.f(e))  es-sends-iff2(es;l;tg;B;ds;e.Q(e);e.f(e))) 

latex

Definitions	x(s), P & Q, A & B, t  T, {T}, P  Q, x:A. B(x), sender(e), 1of(t), E, source(l), loc(e), Id, P  Q, P  Q, rcv(l,tg), kind(e), Knd, Prop, x:A. B(x), e@i. P(e), es-sends-iff2(es;l;tg;B;ds;e.P(e);e.f(e)), ES, IdLnk, x. t(x), a:A fp B(a)
Lemmas	es-sends-iff2 wf, iff wf, fpf wf, IdLnk wf, event system wf, es-E wf, Knd wf, es-kind wf, rcv wf, Id wf, es-loc wf, lsrc wf, es-sender wf, es-kind-rcv